<html>
    <head>
        <title></title>
        <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
        <link rel="stylesheet" type="text/css" href="../style.css">
    </head>
    <body>
        <div class="text">
        <h2>Checks generieren</h2>
        Über die "Checks generieren"-Funktion im Verifikationsmenü lässt sich zu einer
        Prozedur in einem Package eine von der Funktionsweise gleiche Prozedur erzeugen, die
        jedoch zusätzlich noch abfragen bezüglich der in der Prozedur vorhandenen Zusicherungen
        enthält. Dies ist nützlich, wenn geprüft werden soll, bis zu welcher Stelle im 
        zu verifizierenden Programm die Zusicherungen noch stimmen. Bei falscher Zusicherung
        bricht die Programmausführung im Ada-Compiler mit der Ausgabe der entsprechenden
        Zusicherung ab.
        </div>
    </body>
</html>
